{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "d6c335a4",
   "metadata": {},
   "source": [
    "# 10. 分析句子的意思\n",
    "\n",
    "我们已经看到利用计算机的能力来处理大规模文本是多么有用。现在我们已经有了分析器和基于特征的语法，我们能否做一些类似分析句子的意思这样有用的事情？本章的目的是要回答下列问题：\n",
    "\n",
    "1. 我们如何能表示自然语言的意思，使计算机能够处理这些表示？\n",
    "2. 我们怎样才能将意思表示与无限的句子集合关联？\n",
    "3. 我们怎样才能使用程序来连接句子的意思表示到知识的存储？\n",
    "\n",
    "一路上，我们将学习一些逻辑语义领域的形式化技术，看看如何用它们来查询存储了世间真知的数据库。\n",
    "\n",
    "<a href=\"#1-自然语言理解\">1 自然语言理解</a>\n",
    "\n",
    "<a href=\"#3-一阶逻辑\">3 一阶逻辑</a>\n",
    "\n",
    "<a href=\"#4-英语句子的语义\">4 英语句子的语义</a>\n",
    "\n",
    "<a href=\"#5-段落语义层\">5 段落语义层</a>\n",
    "\n",
    "<a href=\"#6-小结\">6 小结</a>\n",
    "\n",
    "<a href=\"#7-深入阅读\">7 深入阅读</a>\n",
    "\n",
    "<a href=\"#8-练习\">8 练习</a>\n",
    "\n",
    "## 1 自然语言理解\n",
    "\n",
    "## 1.1 查询数据库\n",
    "\n",
    "假设有一个程序，让我们输入一个自然语言问题，返回给我们正确的答案："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "44883eff",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "% start S\n",
      "S[SEM=(?np + WHERE + ?vp)] -> NP[SEM=?np] VP[SEM=?vp]\n",
      "VP[SEM=(?v + ?pp)] -> IV[SEM=?v] PP[SEM=?pp]\n",
      "VP[SEM=(?v + ?ap)] -> IV[SEM=?v] AP[SEM=?ap]\n",
      "NP[SEM=(?det + ?n)] -> Det[SEM=?det] N[SEM=?n]\n",
      "PP[SEM=(?p + ?np)] -> P[SEM=?p] NP[SEM=?np]\n",
      "AP[SEM=?pp] -> A[SEM=?a] PP[SEM=?pp]\n",
      "NP[SEM='Country=\"greece\"'] -> 'Greece'\n",
      "NP[SEM='Country=\"china\"'] -> 'China'\n",
      "Det[SEM='SELECT'] -> 'Which' | 'What'\n",
      "N[SEM='City FROM city_table'] -> 'cities'\n",
      "IV[SEM=''] -> 'are'\n",
      "A[SEM=''] -> 'located'\n",
      "P[SEM=''] -> 'in'\n"
     ]
    }
   ],
   "source": [
    "import nltk\n",
    "nltk.data.show_cfg('grammars/book_grammars/sql0.fcfg')"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c4e2a75d",
   "metadata": {},
   "source": [
    "这使我们能够分析SQL查询："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "39fe6ac5",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "SELECT City FROM city_table WHERE Country=\"china\"\n"
     ]
    }
   ],
   "source": [
    "from nltk import load_parser\n",
    "cp = load_parser('grammars/book_grammars/sql0.fcfg')\n",
    "query = 'What cities are located in China'\n",
    "trees = list(cp.parse(query.split()))\n",
    "answer = trees[0].label()['SEM']\n",
    "answer = [s for s in answer if s]\n",
    "q = ' '.join(answer)\n",
    "print(q)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "be03dc29",
   "metadata": {},
   "source": [
    "注意\n",
    "\n",
    "**轮到你来：**设置跟踪为最大，运行分析器，即`cp = load_parser('grammars/book_grammars/sql0.fcfg', trace=3)`，研究当边被完整的加入到图表中时，如何建立`sem`的值。\n",
    "\n",
    "最后，我们在数据库`city.db`上执行查询，检索出一些结果："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "74eab460",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "canton chungking dairen harbin kowloon mukden peking shanghai sian tientsin "
     ]
    }
   ],
   "source": [
    "from nltk.sem import chat80\n",
    "rows = chat80.sql_query('corpora/city_database/city.db', q)\n",
    "for r in rows: print(r[0], end=\" \") "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1cb583f3",
   "metadata": {},
   "source": [
    "由于每行`r`是一个单元素的元组，我们输出元组的成员，而不是元组本身 [# 1](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#tuple-val)。\n",
    "\n",
    "总结一下，我们已经定义了一个任务：计算机对自然语言查询做出反应，返回有用的数据。我们通过将英语的一个小的子集翻译成SQL来实现这个任务们可以说，我们的NLTK代码已经“理解”SQL，只要Python 能够对数据库执行SQL 查询，通过扩展，它也“理解”如What cities are located in China这样的查询。这相当于自然语言理解的例子能够从荷兰语翻译成英语。假设你是一个英语为母语的人，已经开始学习荷兰语。你的老师问你是否理解[(3)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-sem1)的意思："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "65cb1d1c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "negation       \t-\n",
      "conjunction    \t&\n",
      "disjunction    \t|\n",
      "implication    \t->\n",
      "equivalence    \t<->\n"
     ]
    }
   ],
   "source": [
    "nltk.boolean_ops()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "564e0505",
   "metadata": {},
   "source": [
    "从命题符号和布尔运算符，我们可以建立命题逻辑的规范公式（或简称公式）的无限集合。首先，每个命题字母是一个公式。然后，如果φ是一个公式，那么`-`φ也是一个公式。如果φ和ψ是公式，那么`(`φ `&` ψ`)` `(`φ `|` ψ`)` `(`φ `->` ψ`)` `(`φ `<->` ψ`)`也是公式。\n",
    "\n",
    "[2.1](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#tab-boolean-tcs)指定了包含这些运算符的公式为真的条件。和以前一样，我们使用φ和ψ作为句子中的变量，iff作为if and only if（当且仅当）的缩写。\n",
    "\n",
    "表 2.1：\n",
    "\n",
    "命题逻辑的布尔运算符的真值条件。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "c42e31e1",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<NegatedExpression -(P & Q)>"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "read_expr('-(P & Q)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "21d41309",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<AndExpression (P & Q)>"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('P & Q')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "505a67ea",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<OrExpression (P | (R -> Q))>"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('P | (R -> Q)')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "16a195f4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<IffExpression (P <-> --P)>"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr('P <-> -- P')"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c3c5ce14",
   "metadata": {},
   "source": [
    "从计算的角度来看，逻辑给了我们进行推理的一个重要工具。假设你表达Freedonia is not to the north of Sylvania，而你给出理由Sylvania is to the north of Freedonia。在这种情况下，你已经给出了一个论证。句子Sylvania is to the north of Freedonia是论证的假设，而Freedonia is not to the north of Sylvania是结论。从假设一步一步推到结论，被称为推理。通俗地说，就是我们以在结论前面写therefore这样的格式写一个论证。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "53afa15e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "lp = nltk.sem.Expression.fromstring\n",
    "SnF = read_expr('SnF')\n",
    "NotFnS = read_expr('-FnS')\n",
    "R = read_expr('SnF -> -FnS')\n",
    "prover = nltk.Prover9()\n",
    "prover.config_prover9(r'D:/Prover9-Mace4/bin-win32')\n",
    "# 下载 ./asset/Prover9-Mace4.zip 并解压\n",
    "# 或者使用 ./asset/Prover9-Mace4-v05-setup.exe 安装\n",
    "# 可直接指定代码所示路径，或设置为环境变量(可能无效)，不支持中文路径\n",
    "prover.prove(NotFnS, [SnF, R])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ecd85c80",
   "metadata": {},
   "source": [
    "这里有另一种方式可以看到结论如何得出。`SnF -> -FnS`在语义上等价于`-SnF | -FnS`，其中 \"`|`\"是对应于or的二元运算符。在一般情况下，φ`|`ψ在条件*s*中为真，要么φ在*s*中为真，要么ψ在*s*中为真。现在，假设`SnF`和`-SnF | -FnS`都在*s*中为真。如果`SnF`为真，那么`-SnF`不可能也为真；经典逻辑的一个基本假设是：一个句子在一种情况下不能同时为真和为假。因此，`-FnS`必须为真。\n",
    "\n",
    "回想一下，我们解释相对于一个模型的一种逻辑语言的句子，它们是这个世界的一个非常简化的版本。一个命题逻辑的模型需要为每个可能的公式分配值`True`或`False`。我们一步步的来做这个：首先，为每个命题符号分配一个值，然后确定布尔运算符的含义（即[2.1](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#tab-boolean-tcs)）和运用它们到这些公式的组件的值，来计算复杂的公式的值。`估值`是从逻辑的基本符号映射到它们的值。下面是一个例子："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "e337a7a6",
   "metadata": {},
   "outputs": [],
   "source": [
    "val = nltk.Valuation([('P', True), ('Q', True), ('R', False)])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4410d41e",
   "metadata": {},
   "source": [
    "我们使用一个配对的链表初始化一个`估值`，每个配对由一个语义符号和一个语义值组成。所产生的对象基本上只是一个字典，映射逻辑符号（作为字符串处理）为适当的值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "7375d95a",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "val['P']"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "df70cd6e",
   "metadata": {},
   "source": [
    "正如我们稍后将看到的，我们的模型需要稍微更加复杂些，以便处理将在下一节中讨论的更复杂的逻辑形式；暂时的，在下面的声明中先忽略参数`dom`和`g`。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "bcadcc2a",
   "metadata": {},
   "outputs": [],
   "source": [
    "dom = set()\n",
    "g = nltk.Assignment(dom)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "82b21f82",
   "metadata": {},
   "source": [
    "现在，让我们用`val`初始化模型`m`："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "51dbdcf6",
   "metadata": {},
   "outputs": [],
   "source": [
    "m = nltk.Model(dom, val)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9d40b089",
   "metadata": {},
   "source": [
    "每一个模型都有一个`evaluate()`方法，可以确定逻辑表达式，如命题逻辑的公式，的语义值；当然，这些值取决于最初我们分配给命题符号如`P`，`Q`和`R`的真值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "dc34e1bd",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "print(m.evaluate('(P & Q)', g))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "bd5df671",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n"
     ]
    }
   ],
   "source": [
    "print(m.evaluate('-(P & Q)', g))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "4433f10c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n"
     ]
    }
   ],
   "source": [
    "print(m.evaluate('(P & R)', g))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "d4abdfe1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "print(m.evaluate('(P | R)', g))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "03b433ff",
   "metadata": {},
   "source": [
    "注意\n",
    "\n",
    "**轮到你来：**做实验为不同的命题逻辑公式估值。模型是否给出你所期望的值？\n",
    "\n",
    "到目前为止，我们已经将我们的英文句子翻译成命题逻辑。因为我们只限于用字母如`P`和`Q`表示原子句子，不能深入其内部结构。实际上，我们说将原子句子分成主语、宾语和谓词并没有语义上的好处。然而，这似乎是错误的：如果我们想形式化如[(9)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-proplog8)这样的论证，就必须要能“看到里面”基本的句子。因此，我们将超越命题逻辑到一个更有表现力的东西，也就是一阶逻辑。这正是我们下一节要讲的。\n",
    "\n",
    "## 3 一阶逻辑\n",
    "\n",
    "本章的剩余部分，我们将通过翻译自然语言表达式为一阶逻辑来表示它们的意思。并不是所有的自然语言语义都可以用一阶逻辑表示。但它是计算语义的一个不错的选择，因为它具有足够的表现力来表达语义的很多方面，而且另一方面，有出色的现成系统可用于开展一阶逻辑自动推理。\n",
    "\n",
    "下一步我们将描述如何构造一阶逻辑公式，然后是这样的公式如何用来评估模型。\n",
    "\n",
    "<a href=\"#3.1-句法\">3.1 句法</a>\n",
    "\n",
    "<a href=\"#3.2-一阶定理证明\">3.2 一阶定理证明</a>\n",
    "\n",
    "<a href=\"#3.3-一阶逻辑语言总结\">3.3 一阶逻辑语言总结</a>\n",
    "\n",
    "<a href=\"#3.5-独立变星和赋值\">3.5 独立变星和赋值</a>\n",
    "\n",
    "<a href=\"#3.6-量化\">3.6 量化</a>\n",
    "\n",
    "<a href=\"#3.7-量词范围歧义\">3.7 量词范围歧义</a>\n",
    "\n",
    "<a href=\"#3.8-模型的建立\">3.8 模型的建立</a>\n",
    "\n",
    "**vscode jupyter toc**\n",
    "\n",
    "<a href=\"#31-句法\">3.1 句法</a>\n",
    "\n",
    "<a href=\"#32-一阶定理证明\">3.2 一阶定理证明</a>\n",
    "\n",
    "<a href=\"#33-一阶逻辑语言总结\">3.3 一阶逻辑语言总结</a>\n",
    "\n",
    "<a href=\"#35-独立变星和赋值\">3.5 独立变星和赋值</a>\n",
    "\n",
    "<a href=\"#36-量化\">3.6 量化</a>\n",
    "\n",
    "<a href=\"#37-量词范围歧义\">3.7 量词范围歧义</a>\n",
    "\n",
    "<a href=\"#38-模型的建立\">3.8 模型的建立</a>\n",
    "\n",
    "## 3.1 句法\n",
    "\n",
    "一阶逻辑保留所有命题逻辑的布尔运算符。但它增加了一些重要的新机制。首先，命题被分析成谓词和参数，这将我们与自然语言的结构的距离拉近了一步。一阶逻辑的标准构造规则承认以下术语：独立变量和独立常量、带不同数量的参数的谓词。例如，Angus walks可以被形式化为walk(angus)，Angus sees Bertie可以被形式化为see(angus, bertie)。我们称walk为一元谓词，see为二元谓词。作为谓词使用的符号不具有内在的含义，虽然很难记住这一点。回到我们前面的一个例子，[(13a)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-predlog11)和[(13b)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-predlog12)之间没有逻辑区别。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "3ce31f2b",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<ConstantExpression angus>"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "expr = read_expr('walk(angus)', type_check=True)\n",
    "expr.argument"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "3bb930a4",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "e"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.argument.type"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "dbb8a301",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<ConstantExpression walk>"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.function"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "1395dfb0",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<e,?>"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.function.type"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b5c923ad",
   "metadata": {},
   "source": [
    "为什么我们在这个例子的结尾看到`<e,?>`呢？虽然类型检查器会尝试推断出尽可能多的类型，在这种情况下，它并没有能够推断出`walk`的类型，所以其结果的类型是未知的。虽然我们期望`walk`的类型是`<e, t>`，迄今为止类型检查器知道的，在这个上下文中可能是一些其他类型，如`<e, e>`或`<e, <e, t>`。要帮助类型检查器，我们需要指定一个信号，作为一个字典来实施，明确的与非逻辑常量类型关联："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "09418565",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "e"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sig = {'walk': '<e, t>'}\n",
    "expr = read_expr('walk(angus)', signature=sig)\n",
    "expr.function.type"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "60a3d759",
   "metadata": {},
   "source": [
    "一种二元谓词具有类型〈e, 〈e, t〉〉。虽然这是先组合类型e的一个参数成一个一元谓词的类型，我们可以用二元谓词的两个参数直接组合来表示二元谓词。例如，在Angus sees Cyril的翻译中谓词see会与它的参数结合得到结果see(angus, cyril)。\n",
    "\n",
    "在一阶逻辑中，谓词的参数也可以是独立变量，如x，y和z。在NLTK中，我们采用的惯例：*e*类型的变量都是小写。独立变量类似于人称代词，如he，she和it ，其中我们为了弄清楚它们的含义需要知道它们使用的上下文。\n",
    "\n",
    "解释[(14)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-predlog2)中的代名词的方法之一是指向上下文中相关的个体。"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0f2315bc",
   "metadata": {},
   "source": [
    "> ((exists x. dog(x)) -> bark(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c399fb8b",
   "metadata": {},
   "source": [
    "## 3.2 一阶定理证明\n",
    "\n",
    "回顾一下我们较早前在[(10)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-north)中提出的to the north of上的限制："
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3a3bfb28",
   "metadata": {},
   "source": [
    "> all x. all y.(north_of(x, y) -> -north_of(y, x))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ceb91c77",
   "metadata": {},
   "source": [
    "令人高兴的是，定理证明器证明我们的论证是有效的。相反，它得出结论：不能从我们的假设推到出`north_of(f, s)`："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "1c28e9b0",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FnS = read_expr('north_of(f, s)')\n",
    "prover.prove(NotFnS, [SnF, R])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "f6c77706",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "FnS = read_expr('north_of(f, s)')\n",
    "prover.prove(FnS, [SnF, R])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0bcef9df",
   "metadata": {},
   "source": [
    "## 3.3 一阶逻辑语言总结\n",
    "\n",
    "我们将借此机会重新表述前面的命题逻辑的语法规则，并添加量词的形式化规则；所有这些一起组成一阶逻辑的句法。此外，我们会明确相关表达式的类型。我们将采取约定：〈en, t〉一种由n个类型为e的参数组成产生一个类型为t的表达式的谓词的类型。在这种情况下，我们说n是谓词的元数。\n",
    "\n",
    "If P is a predicate of type 〈en, t〉, and α1, αn are terms of type e, then P(α1, αn) is of type t.If α and β are both of type e, then (α = β) and (α != β) are of type t.If φ is of type t, then so is `-`φ.If φ and ψ are of type t, then so are (φ `&` ψ), (φ `|` ψ), (φ `->` ψ) and (φ `<->` ψ).If φ is of type t, and x is a variable of type e, then `exists x.`φ and `all x.`φ are of type t.\n",
    "\n",
    "[3.1](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#tab-nltk-logic)总结了`logic`模块的新的逻辑常量，以及`Expression`模块的两个方法。\n",
    "\n",
    "表 3.1：\n",
    "\n",
    "一阶逻辑所需的新的逻辑关系和运算符总结，以及`Expression`类的两个有用的方法。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "4d324768",
   "metadata": {},
   "outputs": [],
   "source": [
    "dom = {'b', 'o', 'c'}"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7facac37",
   "metadata": {},
   "source": [
    "我们使用工具函数`Valuation.fromstring()`将 symbol `=>` value形式的字符串序列转换成一个`Valuation`对象。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "id": "9aadd009",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{'bertie': 'b',\n",
      " 'boy': {('b',)},\n",
      " 'cyril': 'c',\n",
      " 'dog': {('c',)},\n",
      " 'girl': {('o',)},\n",
      " 'olive': 'o',\n",
      " 'see': {('o', 'c'), ('b', 'o'), ('c', 'b')},\n",
      " 'walk': {('o',), ('c',)}}\n"
     ]
    }
   ],
   "source": [
    "v = \"\"\"\n",
    "bertie => b\n",
    "olive => o\n",
    "cyril => c\n",
    "boy => {b}\n",
    "girl => {o}\n",
    "dog => {c}\n",
    "walk => {o, c}\n",
    "see => {(b, o), (c, b), (o, c)}\n",
    "\"\"\"\n",
    "val = nltk.Valuation.fromstring(v)\n",
    "print(val)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7d0b7036",
   "metadata": {},
   "source": [
    "根据这一估值，`see`的值是一个元组的集合，包含Bertie看到Olive、Cyril 看到Bertie和Olive看到Cyril。\n",
    "\n",
    "注意\n",
    "\n",
    "**轮到你来：**模仿[1.2](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#fig-model-kids)绘制一个图，描述域`m`和相应的每个一元谓词的集合。\n",
    "\n",
    "你可能已经注意到，我们的一元谓词（即`boy`，`girl`，`dog`）也是以单个元组的集合而不是个体的集合出现的。这使我们能够方便的统一处理任何元数的关系。一个形式为P(τ1, τn)的谓词，其中P是n元的，为真的条件是对应于(τ1, τn) 的值的元组属于P的值的元组的集合。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "eee66bd9",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "('o', 'c') in val['see']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "02968688",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "('b',) in val['boy']"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7c32a340",
   "metadata": {},
   "source": [
    "## 3.5 独立变量和赋值\n",
    "\n",
    "在我们的模型，上下文的使用对应的是为变量赋值。这是一个从独立变量到域中实体的映射。赋值使用构造函数`Assignment`，它也以论述的模型的域为参数。我们无需实际输入任何绑定，但如果我们要这样做，它们是以(变量,值)的形式来绑定，类似于我们前面看到的估值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "73b1091f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'x': 'o', 'y': 'c'}"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "g = nltk.Assignment(dom, [('x', 'o'), ('y', 'c')])\n",
    "g"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1add3734",
   "metadata": {},
   "source": [
    "此外，还可以使用`print()`查看赋值，使用与逻辑教科书中经常出现的符号类似的符号："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "id": "fdf06c06",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "g[c/y][o/x]\n"
     ]
    }
   ],
   "source": [
    "print(g)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "eaa6fbcb",
   "metadata": {},
   "source": [
    "现在让我们看看如何为一阶逻辑的原子公式估值。首先，我们创建了一个模型，然后调用`evaluate()`方法来计算真值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "id": "184e640f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m = nltk.Model(dom, val)\n",
    "m.evaluate('see(olive, y)', g)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "5089cae3",
   "metadata": {},
   "source": [
    "这里发生了什么？我们正在为一个公式估值，类似于我们前面的例子`see(olive, cyril)`。然而，当解释函数遇到变量`y`时，不是检查`val`中的值，它在变量赋值`g`中查询这个变量的值："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "id": "7b553195",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'c'"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "g['y']"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1ae2b095",
   "metadata": {},
   "source": [
    "由于我们已经知道`o`和`c`在see关系中表示的含义，所以`True`值是我们所期望的。在这种情况下，我们可以说赋值`g`满足公式`see(olive, y)`。相比之下，下面的公式相对`g`的评估结果为`False`（检查为什么会是你看到的这样）。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "id": "96e9f664",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('see(y, x)', g)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "037df576",
   "metadata": {},
   "source": [
    "在我们的方法中（虽然不是标准的一阶逻辑），变量赋值是部分的。例如，`g`中除了`x`和`y`没有其它变量。方法`purge()`清除一个赋值中所有的绑定。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "id": "6f26fcf3",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{}"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "g.purge()\n",
    "g"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4b93e79e",
   "metadata": {},
   "source": [
    "如果我们现在尝试为公式，如`see(olive, y)`，相对于`g`估值，就像试图解释一个包含一个him的句子，我们不知道him指什么。在这种情况下，估值函数未能提供一个真值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "id": "f8c8397e",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'Undefined'"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('see(olive, y)', g)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e8b4b190",
   "metadata": {},
   "source": [
    "由于我们的模型已经包含了解释布尔运算的规则，任意复杂的公式都可以组合和评估。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "id": "0403a726",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('see(bertie, olive) & boy(bertie) & -walk(bertie)', g)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7e424b6e",
   "metadata": {},
   "source": [
    "确定模型中公式的真假的一般过程称为模型检查。\n",
    "\n",
    "## 3.6 量化\n",
    "\n",
    "现代逻辑的关键特征之一就是变量满足的概念可以用来解释量化的公式。让我们用[(24)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-exists1)作为一个例子。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "id": "14f2f130",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 37,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('exists x.(girl(x) & walk(x))', g)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bfbb4e34",
   "metadata": {},
   "source": [
    "在这里`evaluate()``True`，因为`dom`中有某些*u*通过绑定`x`到*u*的赋值满足（[(25)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-exists2) ）。事实上，`o`是这样一个*u*："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "id": "3bb85ce5",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('girl(x) & walk(x)', g.add('x', 'o'))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e3214b20",
   "metadata": {},
   "source": [
    "NLTK中提供了一个有用的工具是`satisfiers()`方法。它返回满足开放公式的所有个体的集合。该方法的参数是一个已分析的公式、一个变量和一个赋值。下面是几个例子："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "id": "139f7d25",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'b', 'o'}"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fmla1 = read_expr('girl(x) | boy(x)')\n",
    "m.satisfiers(fmla1, 'x', g)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "id": "afcd338f",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'b', 'c', 'o'}"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fmla2 = read_expr('girl(x) -> walk(x)')\n",
    "m.satisfiers(fmla2, 'x', g)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "id": "5d4b5db3",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'b', 'o'}"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fmla3 = read_expr('walk(x) -> girl(x)')\n",
    "m.satisfiers(fmla3, 'x', g)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9fffbc48",
   "metadata": {},
   "source": [
    "想一想为什么`fmla2`和`fmla3`是那样的值，这是非常有用。`->`的真值条件的意思是`fmla2`等价于`-girl(x) | walk(x)`，要么不是女孩要么没有步行的个体满足条件。因为`b`(Bertie)和`c`(Cyril)都不是女孩，根据模型`m`，它们都满足整个公式。当然`o`也满足公式，因为`o`两项都满足。现在，因为话题的域的每一个成员都满足`fmla2`，相应的全称量化公式也为真。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "id": "798c0106",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 42,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "m.evaluate('all x.(girl(x) -> walk(x))', g)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "475bf147",
   "metadata": {},
   "source": [
    "换句话说，一个全称量化公式∀x.φ关于`g`为真，只有对每一个*u*，φ关于`g[u/x]`为真。\n",
    "\n",
    "注意\n",
    "\n",
    "**轮到你来：** 先用笔和纸，然后用`m.evaluate()`，尝试弄清楚`all x.(girl(x) & walk(x))`和`exists x.(boy(x) -> walk(x))`的真值。确保你能理解为什么它们得到这些值。\n",
    "\n",
    "## 3.7 量词范围歧义\n",
    "\n",
    "当我们给一个句子的形式化表示*两*个量词时，会发生什么？"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "id": "ae456256",
   "metadata": {},
   "outputs": [],
   "source": [
    "v2 = \"\"\"\n",
    "bruce => b\n",
    "elspeth => e\n",
    "julia => j\n",
    "matthew => m\n",
    "person => {b, e, j, m}\n",
    "admire => {(j, b), (b, b), (m, e), (e, m)}\n",
    "\"\"\"\n",
    "val2 = nltk.Valuation.fromstring(v2)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e8a5d08f",
   "metadata": {},
   "source": [
    "admire关系可以使用[(28)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-admire-mapping)所示的映射图进行可视化。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "id": "d281a336",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'b', 'e', 'j', 'm'}"
      ]
     },
     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dom2 = val2.domain\n",
    "m2 = nltk.Model(dom2, val2)\n",
    "g2 = nltk.Assignment(dom2)\n",
    "fmla4 = read_expr('(person(x) -> exists y.(person(y) & admire(x, y)))')\n",
    "m2.satisfiers(fmla4, 'x', g2)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "19e45389",
   "metadata": {},
   "source": [
    "这表明`fmla4`包含域中每一个个体。相反，思考下面的公式`fmla5`；没有满足`y`的值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "id": "b251a477",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fmla5 = read_expr('(person(y) & all x.(person(x) -> admire(x, y)))')\n",
    "m2.satisfiers(fmla5, 'y', g2)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "75b2d546",
   "metadata": {},
   "source": [
    "也就是说，没有大家都钦佩的人。看看另一个开放的公式`fmla6`，我们可以验证有一个人，即Bruce，它被Julia和Bruce都钦佩。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "id": "c8f3f2fb",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{'b'}"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "fmla6 = read_expr('(person(y) & all x.((x = bruce | x = julia) -> admire(x, y)))')\n",
    "m2.satisfiers(fmla6, 'y', g2)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "47398736",
   "metadata": {},
   "source": [
    "注意\n",
    "\n",
    "**轮到你来：**基于`m2`设计一个新的模型，使[(27a)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-scope2a)在你的模型中为假；同样的，设计一个新的模型使[(27b)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-scope2b)为真。\n",
    "\n",
    "## 3.8 模型的建立\n",
    "\n",
    "我们一直假设我们已经有了一个模型，并要检查模型中的一个句子的真值。相比之下，模型的建立是给定一些句子的集合，尝试创造一种新的模型。如果成功，那么我们知道集合是一致的，因为我们有模型的存在作为证据。\n",
    "\n",
    "我们通过创建`Mace()`的一个实例并调用它的`build_model()`方法来调用Mace4模式产生器，与调用Prover9定理证明器类似的方法。一种选择是将我们的候选的句子集合作为假设，保留目标为未指定。下面的交互显示了`[a, c1]`和`[a, c2]`都是一致的列表，因为Mace成功的为它们都建立了一个模型，而`[c1, c2]`不一致。"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b2d0914b",
   "metadata": {},
   "source": [
    "<!--https://stackoverflow.com/questions/25844794/nltk-was-unable-to-find-mace4/44805638#44805638-->\n",
    "\n",
    "**在执行以下几段代码时可能会出现找不到 mace5.exe 的情况，此时需要在 nltk 安装包目录的 `nltk/inference/prover9.py` 文件的 `binary_locations(self)` 函数中添加当前 `Prover9-Mace4\\bin-win32` 目录的绝对路径。添加路径后部分结果应该如下：**\n",
    "\n",
    "```\n",
    "return [\n",
    "    \"D:\\\\Prover9-Mace4\\\\bin-win32\",\n",
    "    \"/usr/local/bin/prover9\",\n",
    "    \"/usr/local/bin/prover9/bin\",\n",
    "    \"/usr/local/bin\",\n",
    "    \"/usr/bin\",\n",
    "    \"/usr/local/prover9\",\n",
    "    \"/usr/local/share/prover9\",\n",
    "]\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "9446d3f9",
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "a3 = read_expr('exists x.(man(x) & walks(x))')\n",
    "c1 = read_expr('mortal(socrates)')\n",
    "c2 = read_expr('-mortal(socrates)')\n",
    "mb = nltk.Mace(5)\n",
    "print(mb.build_model(None, [a3, c1]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "ca6d678c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "a3 = read_expr('exists x.(man(x) & walks(x))')\n",
    "c1 = read_expr('mortal(socrates)')\n",
    "c2 = read_expr('-mortal(socrates)')\n",
    "mb = nltk.Mace(5)\n",
    "print(mb.build_model(None, [a3, c1]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "e2593140",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "print(mb.build_model(None, [a3, c2]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "18569d6f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n"
     ]
    }
   ],
   "source": [
    "print(mb.build_model(None, [c1, c2]))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1eee1222",
   "metadata": {},
   "source": [
    "我们也可以使用模型建立器作为定理证明器的辅助。假设我们正试图证明`S` ⊢ `g`，即`g`是假设`S = [s1, s2, ..., sn]`的逻辑派生。我们可以同样的输入提供给Mace4，模型建立器将尝试找出一个反例，就是要表明`g`*不*遵循从`S`。因此，给定此输入，Mace4将尝试为假设`S`连同`g`的否定找到一个模型，即列表`S' = [s1, s2, ..., sn, -g]`。如果`g`从`S`不能证明出来，那么Mace4会返回一个反例，比Prover9更快的得出结论：无法找到所需的证明。相反，如果`g`从`S`是可以证明出来，Mace4 可能要花很长时间不能成功地找到一个反例模型，最终会放弃。\n",
    "\n",
    "让我们思考一个具体的方案。我们的假设是列表[There is a woman that every man loves, Adam is a man, Eve is a woman]。我们的结论是Adam loves Eve。Mace4能找到使假设为真而结论为假的模型吗？在下面的代码中，我们使用`MaceCommand()`检查已建立的模型。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "b64d7f7c",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a4 = read_expr('exists y. (woman(y) & all x. (man(x) -> love(x,y)))')\n",
    "a5 = read_expr('man(adam)')\n",
    "a6 = read_expr('woman(eve)')\n",
    "g = read_expr('love(adam,eve)')\n",
    "mc = nltk.MaceCommand(g, assumptions=[a4, a5, a6])\n",
    "mc.build_model()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b993c05d",
   "metadata": {},
   "source": [
    "因此答案是肯定的：Mace4发现了一个反例模型，其中Adam爱某个女人而不是Eve。但是，让我们细看Mace4的模型，转换成我们用来估值的格式。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "62bbf74e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{'C1': 'b',\n",
      " 'adam': 'a',\n",
      " 'eve': 'a',\n",
      " 'love': {('a', 'b')},\n",
      " 'man': {('a',)},\n",
      " 'woman': {('a',), ('b',)}}\n"
     ]
    }
   ],
   "source": [
    "print(mc.valuation)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6d694e25",
   "metadata": {},
   "source": [
    "这个估值的一般形式应是你熟悉的：它包含了一些单独的常量和谓词，每一个都有适当类型的值。可能令人费解的是`C1`。它是一个“Skolem 常量”，模型生成器作为存在量词的表示引入的。也就是说，模型生成器遇到`a4`里面的`exists y`，它知道，域中有某个个体`b`满足`a4`中的开放公式。然而，它不知道`b`是否也是它的输入中的某个地方的一个独立常量的标志，所以它为`b`凭空创造了一个新名字，即`C1`。现在，由于我们的假设中没有关于独立常量`adam`和`eve`的信息，模型生成器认为没有任何理由将它们当做表示不同的实体，于是它们都得到映射到`a`。此外，我们并没有指定`man`和`woman`表示不相交的集合，因此，模型生成器让它们相互重叠。这个演示非常明显的隐含了我们用来解释我们的情境的知识，而模型生成器对此一无所知。因此，让我们添加一个新的假设，使man和woman不相交。模型生成器仍然产生一个反例模型，但这次更符合我们直觉的有关情况："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "04ca0beb",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a7 = read_expr('all x. (man(x) -> -woman(x))')\n",
    "g = read_expr('love(adam,eve)')\n",
    "mc = nltk.MaceCommand(g, assumptions=[a4, a5, a6, a7])\n",
    "mc.build_model()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "612d93c5",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{'C1': 'c',\n",
      " 'adam': 'a',\n",
      " 'eve': 'b',\n",
      " 'love': {('a', 'c')},\n",
      " 'man': {('a',)},\n",
      " 'woman': {('b',), ('c',)}}\n"
     ]
    }
   ],
   "source": [
    "print(mc.valuation)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "13d82fc6",
   "metadata": {},
   "source": [
    "经再三考虑，我们可以看到我们的假设中没有说Eve是论域中唯一的女性，所以反例模型其实是可以接受的。如果想排除这种可能性，我们将不得不添加进一步的假设，如`exists y. all x. (woman(x) -> (x = y))`以确保模型中只有一个女性。\n",
    "\n",
    "## 4 英语句子的语义\n",
    "\n",
    "## 4.1 基于特征的语法中的合成语义学\n",
    "\n",
    "在本章开头，我们简要说明了一种在句法分析的基础上建立语义表示的方法，使用在[9.](https://usyiyi.github.io/nlp-py-2e-zh/9.html#chap-featgram)开发的语法框架。这一次，不是构建一个SQL查询，我们将建立一个逻辑形式。我们设计这样的语法的指导思想之一是组合原则。（也称为Frege原则；下面给出的公式参见[(Gleitman & Liberman, 1995)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#partee1995lsc) 。）\n",
    "\n",
    "**组合原则**：整体的含义是部分的含义与它们的句法结合方式的函数。\n",
    "\n",
    "我们将假设一个复杂的表达式的语义相关部分由句法分析理论给出。在本章中，我们将认为表达式已经用上下文无关语法分析过。然而，这不是组合原则的内容。\n",
    "\n",
    "我们现在的目标是以一种可以与分析过程平滑对接的方式整合语义表达的构建。[(29)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-sem3)说明了我们想建立的这种分析的第一个近似。\n",
    "\n",
    "\n",
    "> VP[SEM=?v] -> IV[SEM=?v]\n",
    "> \n",
    "> NP[SEM=<cyril>] -> 'Cyril'\n",
    "> \n",
    "> IV[SEM=<\\x.bark(x)>] -> 'barks'\n",
    "\n",
    "<a href=\"#4.1-基于特征的语法中的合成语义学\">4.1 基于特征的语法中的合成语义学</a>\n",
    "\n",
    "<a href=\"#4.2-λ演算\">4.2 λ演算</a>\n",
    "\n",
    "<a href=\"#4.3-量化的NP\">4.3 量化的NP</a>\n",
    "\n",
    "<a href=\"#4.5-再述量词歧义\">4.5 再述量词歧义</a>\n",
    "\n",
    "**vscode jupyter toc**\n",
    "\n",
    "<a href=\"#41-基于特征的语法中的合成语义学\">4.1 基于特征的语法中的合成语义学</a>\n",
    "\n",
    "<a href=\"#42-λ演算\">4.2 λ演算</a>\n",
    "\n",
    "<a href=\"#43-量化的NP\">4.3 量化的NP</a>\n",
    "\n",
    "<a href=\"#45-再述量词歧义\">4.5 再述量词歧义</a>\n",
    "\n",
    "\n",
    "## 4.2 λ演算\n",
    "\n",
    "在[3](https://usyiyi.github.io/nlp-py-2e-zh/1.html#sec-computing-with-language-simple-statistics)中，我们指出数学集合符号对于制定我们想从文档中选择的词的属性P很有用。我们用[(31)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-set-comprehension-math2)说明这个，它是“所有w的集合，其中w是V（词汇表）的元素且w有属性P”的表示。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "1fccf1dc",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<LambdaExpression \\x.(walk(x) & chew_gum(x))>"
      ]
     },
     "execution_count": 59,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "expr = read_expr(r'\\x.(walk(x) & chew_gum(x))')\n",
    "expr"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "2dd0b959",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "set()"
      ]
     },
     "execution_count": 60,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr.free()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d4d8efc1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\x.(walk(x) & chew_gum(y))\n"
     ]
    }
   ],
   "source": [
    "print(read_expr(r'\\x.(walk(x) & chew_gum(y))'))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "bf9add5a",
   "metadata": {},
   "source": [
    "我们对绑定表达式中的变量的结果有一个特殊的名字：λ-抽象。当你第一次遇到λ-抽象时，很难对它们的意思得到一个直观的感觉。[(33b)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-walk-chewgum12)的一对英语表示是“是一个x，其中x步行且x嚼口香糖”或“具有步行和嚼口香糖的属性。”通常认为λ-抽象可以很好的表示动词短语（或无主语从句），尤其是当它作为参数出现在它自己的右侧时。如[(34a)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-walk-chewgum21)和它的翻译[(34b)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-walk-chewgum22)中的演示。\n",
    "\n",
    "> (walk(x) & chew_gum(x))[gerald/x]\n",
    "\n",
    "虽然我们迄今只考虑了λ-抽象的主体是一个某种类型t的开放公式，这不是必要的限制；主体可以是任何符合语法的表达式。下面是一个有两个λ的例子。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "38e81ce9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\y.(dog(cyril) & own(y,cyril))\n"
     ]
    }
   ],
   "source": [
    "print(read_expr(r'\\x.\\y.(dog(x) & own(y, x))(cyril)').simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "430e6170",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(dog(cyril) & own(angus,cyril))\n"
     ]
    }
   ],
   "source": [
    "print(read_expr(r'\\x y.(dog(x) & own(y, x))(cyril, angus)').simplify()) "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e3549168",
   "metadata": {},
   "source": [
    "我们所有的λ-抽象到目前为止只涉及熟悉的一阶变量：`x`、`y`等——类型*e*的变量。但假设我们要处理一个抽象，例如`\\x.walk(x)`作为另一个λ-抽象的参数？我们不妨试试这个：\n",
    "\n",
    "> \\y.y(angus)(\\x.walk(x))\n",
    "\n",
    "当β-约减在一个应用`f(a)`中实施时，我们检查是否有自由变量在`a`同时也作为`f`的子术语中绑定的变量出现。假设在上面讨论的例子中，`x`是`a`中的自由变量，`f`包括子术语`exists x.P(x)`。在这种情况下，我们产生一个`exists x.P(x)`的字母变体，也就是说，`exists z1.P(z1)`，然后再进行约减。这种重新标记由`logic`中的β-约减代码自动进行，可以在下面的例子中看到的结果。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "60e38b77",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(\\P.exists x.P(x))(\\y.see(y,x))\n"
     ]
    }
   ],
   "source": [
    "expr3 = read_expr('\\P.(exists x.P(x))(\\y.see(y, x))')\n",
    "print(expr3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ea63bc32",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "exists z1.see(z1,x)\n"
     ]
    }
   ],
   "source": [
    "print(expr3.simplify())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f6a49607",
   "metadata": {},
   "source": [
    "注意\n",
    "\n",
    "当你在下面的章节运行这些例子时，你可能会发现返回的逻辑表达式的变量名不同；例如你可能在前面的公式的`z1`的位置看到`z14`。这种标签的变化是无害的——事实上，它仅仅是一个字母变体的例子。\n",
    "\n",
    "在此附注之后，让我们回到英语句子的逻辑形式建立的任务。\n",
    "\n",
    "## 4.3 量化的NP\n",
    "\n",
    "在本节开始，我们简要介绍了如何为Cyril barks构建语义表示。你会以为这太容易了——肯定还有更多关于建立组合语义的。例如，量词？没错，这是一个至关重要的问题。例如，我们要给出[(42a)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-sem5a)的逻辑形式[(42b)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-sem5b)。如何才能实现呢？"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "b6e1ba8f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(\\X x.X(\\y.chase(x,y)))(\\P.exists x.(dog(x) & P(x)))\n"
     ]
    }
   ],
   "source": [
    "read_expr = nltk.sem.Expression.fromstring\n",
    "tvp = read_expr(r'\\X x.X(\\y.chase(x,y))')\n",
    "np = read_expr(r'(\\P.exists x.(dog(x) & P(x)))')\n",
    "vp = nltk.sem.ApplicationExpression(tvp, np)\n",
    "print(vp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "09a2464a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\\x.exists z2.(dog(z2) & chase(x,z2))\n"
     ]
    }
   ],
   "source": [
    "print(vp.simplify())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "58a28e2f",
   "metadata": {},
   "source": [
    "为了建立一个句子的语义表示，我们也需要组合主语`NP`的语义。如果后者是一个量化的表达式，例如every girl，一切都与我们前面讲过的a dog barks一样的处理方式；主语转换为函数表达式，这被用于`VP`的语义表示。然而，我们现在似乎已经用适当的名称为自己创造了另一个问题。到目前为止，这些已经作为单独的常量进行了语义的处理，这些不能作为像[(47)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-sem99)那样的表达式的函数应用。因此，我们需要为它们提出不同的语义表示。我们在这种情况下所做的是重新解释适当的名称，使它们也成为如量化的`NP`那样的函数表达式。这里是Angus的λ表达式。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "d11c8143",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "all z4.(dog(z4) -> exists z3.(bone(z3) & give(angus,z3,z4)))\n"
     ]
    }
   ],
   "source": [
    "from nltk import load_parser\n",
    "parser = load_parser('grammars/book_grammars/simple-sem.fcfg', trace=0)\n",
    "sentence = 'Angus gives a bone to every dog'\n",
    "tokens = sentence.split()\n",
    "for tree in parser.parse(tokens):\n",
    "    print(tree.label()['SEM'])"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "89e7f9a8",
   "metadata": {},
   "source": [
    "NLTK提供一些实用工具使获得和检查的语义解释更容易。函数`interpret_sents()`用于批量解释输入句子的列表。它建立一个字典`d`，其中对每个输入的句子`sent`，`d[sent]`是包含`sent`的分析树和语义表示的(*synrep*, *semrep*)对的列表。该值是一个列表，因为`sent`可能有句法歧义；在下面的例子中，列表中的每个句子只有一个分析树。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "94a4607a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(S[SEM=<walk(irene)>]\n",
      "  (NP[-LOC, NUM='sg', SEM=<\\P.P(irene)>]\n",
      "    (PropN[-LOC, NUM='sg', SEM=<\\P.P(irene)>] Irene))\n",
      "  (VP[NUM='sg', SEM=<\\x.walk(x)>]\n",
      "    (IV[NUM='sg', SEM=<\\x.walk(x)>, TNS='pres'] walks)))\n",
      "(S[SEM=<exists z5.(ankle(z5) & bite(cyril,z5))>]\n",
      "  (NP[-LOC, NUM='sg', SEM=<\\P.P(cyril)>]\n",
      "    (PropN[-LOC, NUM='sg', SEM=<\\P.P(cyril)>] Cyril))\n",
      "  (VP[NUM='sg', SEM=<\\x.exists z5.(ankle(z5) & bite(x,z5))>]\n",
      "    (TV[NUM='sg', SEM=<\\X x.X(\\y.bite(x,y))>, TNS='pres'] bites)\n",
      "    (NP[NUM='sg', SEM=<\\Q.exists x.(ankle(x) & Q(x))>]\n",
      "      (Det[NUM='sg', SEM=<\\P Q.exists x.(P(x) & Q(x))>] an)\n",
      "      (Nom[NUM='sg', SEM=<\\x.ankle(x)>]\n",
      "        (N[NUM='sg', SEM=<\\x.ankle(x)>] ankle)))))\n"
     ]
    }
   ],
   "source": [
    "sents = ['Irene walks', 'Cyril bites an ankle']\n",
    "grammar_file = 'grammars/book_grammars/simple-sem.fcfg'\n",
    "for results in nltk.interpret_sents(sents, grammar_file):\n",
    "    for (synrep, semrep) in results:\n",
    "        print(synrep)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9e00ec4d",
   "metadata": {},
   "source": [
    "现在我们已经看到了英文句子如何转换成逻辑形式，前面我们看到了在模型中如何检查逻辑形式的真假。把这两个映射放在一起，我们可以检查一个给定的模型中的英语句子的真值。让我们看看前面定义的模型`m`。工具`evaluate_sents()`类似于`interpret_sents()`，除了我们需要传递一个模型和一个变量赋值作为参数。输出是三元组(*synrep*, *semrep*, *value*)，其中*synrep*、*semrep*和以前一样，*value*是真值。为简单起见，下面的例子只处理一个简单的句子。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "0166e721",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "all z6.(boy(z6) -> see(cyril,z6))\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "v = \"\"\"\n",
    "bertie => b\n",
    "olive => o\n",
    "cyril => c\n",
    "boy => {b}\n",
    "girl => {o}\n",
    "dog => {c}\n",
    "walk => {o, c}\n",
    "see => {(b, o), (c, b), (o, c)}\n",
    "\"\"\"\n",
    "val = nltk.Valuation.fromstring(v)\n",
    "g = nltk.Assignment(val.domain)\n",
    "m = nltk.Model(val.domain, val)\n",
    "sent = 'Cyril sees every boy'\n",
    "grammar_file = 'grammars/book_grammars/simple-sem.fcfg'\n",
    "results = nltk.evaluate_sents([sent], grammar_file, m, g)[0]\n",
    "for (syntree, semrep, value) in results:\n",
    "    print(semrep)\n",
    "    print(value)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ffb66783",
   "metadata": {},
   "source": [
    "## 4.5 再述量词歧义\n",
    "\n",
    "上述方法的一个重要的限制是它们没有处理范围歧义。我们的翻译方法是句法驱动的，认为语义表示与句法分析紧密耦合，语义中量词的范围也因此反映句法分析树中相应的`NP`的相对范围。因此，像[(26)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-scope1)这样的句子，在这里重复，总是会被翻译为[(53a)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-scope12a)而不是[(53b)](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#ex-scope12b)。\n",
    "\n",
    "\n",
    "> \\P.exists y.(dog(y) & P(y))(\\z2.chase(z1,z2))\n",
    "\n",
    "最后，我们调用`s_retrieve()`检查读法。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "71aac434",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "chase(z2,z3)\n"
     ]
    }
   ],
   "source": [
    "# cs_semrep.s_retrieve(trace=True) # 过时版本的代码\n",
    "\n",
    "from nltk.sem import cooper_storage as cs\n",
    "sentence = 'every girl chases a dog'\n",
    "trees = cs.parse_with_bindops(sentence, grammar='grammars/book_grammars/storage.fcfg')\n",
    "semrep = trees[0].label()['SEM']\n",
    "cs_semrep = cs.CooperStore(semrep)\n",
    "print(cs_semrep.core)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ac39bdb5",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "bo(\\P.all x.(girl(x) -> P(x)),z2)\n",
      "bo(\\P.exists x.(dog(x) & P(x)),z3)\n"
     ]
    }
   ],
   "source": [
    "for bo in cs_semrep.store:\n",
    "    print(bo)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "02f06d53",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Permutation 1\n",
      "   (\\P.all x.(girl(x) -> P(x)))(\\z2.chase(z2,z3))\n",
      "   (\\P.exists x.(dog(x) & P(x)))(\\z3.all x.(girl(x) -> chase(x,z3)))\n",
      "Permutation 2\n",
      "   (\\P.exists x.(dog(x) & P(x)))(\\z3.chase(z2,z3))\n",
      "   (\\P.all x.(girl(x) -> P(x)))(\\z2.exists x.(dog(x) & chase(z2,x)))\n"
     ]
    }
   ],
   "source": [
    "cs_semrep.s_retrieve(trace=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "37eece89",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "exists x.(dog(x) & all z5.(girl(z5) -> chase(z5,x)))\n",
      "all x.(girl(x) -> exists z6.(dog(z6) & chase(x,z6)))\n"
     ]
    }
   ],
   "source": [
    "for reading in cs_semrep.readings:\n",
    "    print(reading)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c10979e0",
   "metadata": {},
   "source": [
    "## 5 段落语义层\n",
    "\n",
    "段落是句子的序列。很多时候，段落中的一个句子的解释依赖它前面的句子。一个明显的例子来自照应代词，如he、she和it。给定一个段落如Angus used to have a dog. But he recently disappeared.，你可能会解释he指的是Angus的狗。然而，在Angus used to have a dog. He took him for walks in New Town.中，你更可能解释he指的是Angus自己。\n",
    "\n",
    "## 5.1 段落表示理论\n",
    "\n",
    "一阶逻辑中的量化的标准方法仅限于单个句子。然而，似乎是有量词的范围可以扩大到两个或两个以上的句子的例子。。我们之前看到过一个，下面是第二个例子，与它的翻译一起。\n",
    "\n",
    "> ([x, y], [angus(x), dog(y), own(x,y)])\n",
    "\n",
    "我们可以使用`draw()`方法 [# 1](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#draw-drs)可视化结果，如[5.2](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#fig-drs-screenshot)所示。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "8c2b46d2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([x,y],[angus(x), dog(y), own(x,y)])\n"
     ]
    }
   ],
   "source": [
    "# drs1.draw() # 1 过时版本的代码\n",
    "# https://www.nltk.org/book/ch10.html\n",
    "import nltk \n",
    "\n",
    "read_dexpr = nltk.sem.DrtExpression.fromstring\n",
    "drs1 = read_dexpr('([x, y], [angus(x), dog(y), own(x, y)])') # [1]\n",
    "print(drs1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "492beff4",
   "metadata": {},
   "outputs": [],
   "source": [
    "drs1.draw() # 执行后弹出一个窗口"
   ]
  },
  {
   "attachments": {
    "66d94cb86ab90a95cfe745d9613c37b1.png": {
     "image/png": "iVBORw0KGgoAAAANSUhEUgAAAGoAAABuCAYAAADPsIaBAAACHGlDQ1BpY2MAAHjardK/axNhGMDx713QFpQoIQgVlKOoVIgamiUi0rRJa2NDjElK22zXu2tyend9ubu2RhyK+heIKOKkgjgITlIRkQwODjqIoMHJqZNOhSxS43BeAkJ18YEXPs/Dw/vj4YXIV1UISwZsx3fL5yaU+YWaMtBGYogYQ5xSNU+Ml0oFdozOJySAjydUIayHww867zZHxr4t3dicWT/9nb9H1J1fqIGUAOL1wBkgvhi4CsTXfOGD1ADiWkPVQboGJNxqOQvSEyBaD/wCiC4GfgtEV7W6D1IbSDq66YA8CKR1w9NAzgCW7mk2yE+BTdte1iFyGxjRhOtD5BVwZH6hpgRXXqvD2ZsQud+v1Q7Bs5dwsNCvHb0IsTY8H+vXttpIgHRg0FtKjQIg7dmAXXe63a05GDgO25+73R8b3e72Y4h8gVZHW3FXf89Lkt7Dv/LgzUEOH/xQOzmYCwBJeNSCWSDfgnstOHYXYmeglIFqBjmVClcwQwBiWdMxbFWZzik50xOW2uT/hm2thGftA/Y6i8ULwDDwxlutTIZeMqfyoXU1NxP6aiNb7PW4U+XQl9TzpdCGM1sJLfyJXo/hTVb6+1TnQl9enun16EaudwfHKhZCm36+GposJg4GNioK0+RQyGHiIbBQaULw/wB274dbh+Wfcvq1cn39z3n4xhUfILssmq5Zb/jKuBCWkVDyjnYyoYwmk2l+ARzCr54kUA+4AAAABmJLR0QA/wD/AP+gvaeTAAAACXBIWXMAAAsSAAALEgHS3X78AAAACXZwQWcAAABqAAAAbgBHw9ccAAAW3klEQVR42u2de3RUVZq3n1Pn1C2VkKQSciMXSACJCXJHIul0oPGCoD2IKK1cRBfTzjgjLrs/nenVrdPzda9uoZvusRmXLJZNRwW5yF2kISIIogzSgxguCSEEQsiFXKBCbpVU1fv9EVMSSFUqMf0lFetZK2txzt7nrbPPr867z96/2gcFGPf888+Pvf/++6cnJSVlGY3GREVRCNA3iAiKotDU1FRSWlp6eO/evR//8Y9//FJ54YUXnn7sscf+xWg0jrPb7bhcrr4+1wCATqfDYDDQ0tLy5aZNm/6kZWVlTQfGNTQ09PW5BbgJl8uFw+FA07Sx2dnZ07XIyMislpaWvj6vAB5oaWnBarVmaSKS0FW6ExFaW1uprajgxK7dVJw+jb2uDgDjoEHEpKUx7qFZWGNi0Ov1+NLH3Rzz9K6dXD2dh932dczQUKLS0kl76OEexaysquDDQ7vILz5NXYMNESHEMog7k9N5MOthogf7HrM/oChKgvLRRx9JV4232+3k7f+YY395m2CjkcFRg4kcMgQRoebKFa5eraKhpYXJTy1i9A+mYzQavV6E9pgFB/Zz9r0cgowGomJjCBuSCIrC9SuXuVpeTmOzndQfLeaOaT/wOeaBox+x7sO/YArWEzkkkqjB0TidTiqvllNTVktro5MnZy1h2pQZHmI28fk7q/mkBkxf7zGGRJAwIp2MKeOIMLTta6n8grfWHsH+TSXuypzJ9NFxtJR9zso3P8FkbSs0Go1gt2MHaG6mefA9LHsmC3M3xFIXLFjwHyKCp7/W1lZOfXyA42veItFsZkpSIvc+/DAPvvwSkx+4jzh7C0FVV7E31JN/9Bh6q5XIpER0Op3XmIUH93N+3WpSBpuYNmUYmXNnkvnPzzN25r0MszqJcdXQarvOhaOfwyArYYlJXcY8+D/7ydm5mtB4E2OzUnh01iMsm/9TpmV8H721GXtQLXX19Rz94ijhwREkxnYW08W5jf/B2w0juDdtKGbFzhfr32P3J7m8v66GqXPvJkwTWqvP8ov/WgsjJjM+vIl1G7dyeO82lLGzSY8QyquaiYiOIEwpI2fjh5xlBPeOH0pYSAghMUNJHxaJ4uW63/qnOZ1Or0rWVFRw8p11jAwyM9liIcHpwlpWhuvcOcTlxFpexmiXi/AgC8dEOPnOOuLS7mRwXJzHmNcqyindnsNdQy3cPTqSQTFGzGodUlcBOh1BOhvDEg1Y9YP5nzyhcHsOg1PTiIgb4jFmxdVyNnz4FyKTLaRPiyVqsIVWo42rjSU0ttTjCmogbngIRmscZw5WsOHDv5CanEZczK0xnSjA5AeW8PQ/DEPRqSz7t//DkTf/nWdX7Wb51mxWzU/HpdcBMH/Jv/DDFDP/uPgB5t37r5y+VIk6djz//GIG4hKQy1x69wCN85fw9A+HgaKgOJupqrbh/cp3pEuh8vfmEi5CZnAw8QiDbtRhPnUKFy5wCUFnzqDU38CggMFiwXajnvy9uVgXLfAY88rBPURYhGkZcRhDTehDdGjOChyXPwVFh+oowxiqI1wXwrRgjdqPS7hycA9hjy/xGHP/539FNQoTZycREm5CbxSqXZf4suogrS479WoV5nA90ZZQgmYbOfznIvZ//leeePip24RyAdJQQ3l5e15TSV/87zy372P+OyeXoh+mEuds69fra0ooNwWh6EMZAVxVNVobr1HWeK3t0NZK6oGG+pvjdR+tqwcJrbiYMUFBJOh0RCgKQQj6a7XovjgOgL65GSNgUHUoLmFMUBBXiou9jsdCqs8yLM2KOSoEY5gZfYgRzexE13oBUFBDHGiaBS1IRWfUGJdm5WJNvteYJdfPkTxpMNHx4WgGFU3VoajNVDkKEZegmZ0EG8w4nUbMQSaGTRxMScW5TmJ+02V/U+aitlzH1Mem8d+/agGnC2mv5nDhar7Gmdwd7AZeGBnTMeZNTwDfZoza5R1lsdURo9cINxkJUVUMmoaq10DVQAGMBjSHA9XhwOVwEqPYsdnq8BbXqm8gKj4S0+AQjOFB6C1GdCYNnaoiCDiC0OwGVLMBRa8RFd+Erb7aa8x6Vx1pydEEBweh13Roqg5N1/YHQqtLxeFy4XC6cBhcxCZbOVtW0UlMJy4BcbluKWukurYUiEMTJ86vL/rK5+az8usaL6zeyeMjVCpsNw13nC6EzuL1slCqpmLUqwSHhGA0GlHNJhSLBcxmUBRobkZpbERpaiK42Y5JuYHqEq8n5dSr6EJMGK3BGMLMqEEGdEYNvs77OFwodgeKQWtLhSF1OPWq15h6TcVkMhJsMqFXdRhUFbOmx6RqCEKz00FTqwO704lDdWE2GtBUrVOhBEBuv7CqIQ6ox+504nS23SrP/mkL05q28PhL66m9WsWViNCO4drvIvk7C2WIjaWhphp9WBg6iwUldBCEhUFICIqiIA0NKNevo6urQ19fT4PdjsEa4fWkWoIjqHeBNsiMGmxGZ9ajmNRvhGp1oWoa6FQ0F9xwQWtwBJqXmDHWWJqut2DSDJg0jSC9RrDehFkzAUKDoxlNZ0dztGJ3OGiytRJtje1cKAERXceyhkK2/PET+P6/McTgpPnr3Bei6giZuJT/+8h6fvGLZwhd+Q6ZQww3hWsTSr6tUF3lzUF33UXpwQO0hoViCguD8HCwWlEGDWqrUN8ARiOKwUCrpudKRSUho9O95mM1fjQlVccZb9SjMxtQTBoYdCh6HSiC6HSg6NChIHYnJVX16BImeI1559BxHL/wEapTJchkwKI3EWwwYVZNCKAoOkQUQMHRLFRcuM7klBmd9lEC2GpKKC23o+LkWukZNv/uLc4wgf96YQZKc1XbEx3Q1HodW2Ur9/zT28zcuog/vZhD/NvPkKj/OpzL5b5D/659VGTmPdjy8jjmcjEtPBzVam0Ty2JpS316PSjgAr6ovQaRg4mceg/Xm5o8xrSOf4Arf/0bX+ZXcPf3RoJeRafXIUrbzLGi6XCJAk74Kr+ChhaIG/cA15s8T3Xdfcf3OV1yhHPHy8nIHoFBp0evM6DqNATQK3oMOid6XBQcK8asmbh7VDaNN5pvieREs8D5db/hJ+u+2fsP//if/Of8GQRfL6baKYhOA0AvKk5nC+U14Tyf8zJ7Fr/Gy+/dxdonx6MHcOnaBraafKs7SsnJyfE6M2E2m9EqKqn+9DCjhyUzNjEBQ2hohz6q1VbHl6WXOXWhmIh7MmiNjqbJi1BmsxmpPo+t8H0mZA7nrgmJqIa2uwkUEHC2uMg7cZn//fQ8g1LmQuTwLmPW2Ms4eHodd41LJH1sIiFmM0bVgCDYnS3caGziqxOX+Op/S/jBXQuJMMZ1ElNPbMowQtSOe1ub6qiqqKC+tW1bDYklJTaE+spiymxtOw2hcQyNDgb7NYouVbWNk9RBJKfEoNRXUlRm67lQa9eu9SqUqqpYrVacJSVc//IkcUOTGBIRwaCv76i6xkbKamoov1TCoNHpqImJ1NbWev32tMdsLD1F3cUPGHpHOMkjoggLbxPfdq2Ri0VVFBdcIzhhFkHx6T7HLKsr5ljRVmJjQhiSEEFoqAUQrl1v4EpJNeUVN5gy4lHiBg3rMmZ/Qnnrrbekq0qqqhIREUGEJZiSTz+F+nrMQUEoikJjYyNKsIWEqZnUNNRTU1PjU+PbY4ZZTJw7uh2t9RKhIU5QoO6GhkNLYsSUH3K9obnbMUPCLHx2JpeahvPo9M0ggrPVTKQlhXvS7uPG9QafY/YXlDVr1nQpFLQZWSaTicjISMLCwtomGgG73c7169eprq6mubm5Wx2mv8TsDyirV6/2Sah2VFVFp9O5Z51FBNe3HMz5S8y+pMvH81v5e3wT/SVmX6JkZ2d3644K0DcoIhIQyg/Q9fUJBPCNgFB+QkAoPyEglJ8QEMpPCAjlJwSE8hMCQvkJmqcCf/m5b0/xt3G+5q3Q3xrjK/74JQykPj8hIJSfEBDKTwgI5Sf4JNSKFSt46qmn3NsLFy4kJyenQ51nn32W9evXu7c3btzIc88919ftGzD4JNSSJUv44IMP2LZtGxs2bODIkSPMmzevQ5077riDd99917397rvvMmrUqL5u38BBPHBr0dq1ayUpKUni4uJk7969t9UvKSkRs9ks9fX10tDQIEFBQVJaWir9ES/N7rd4dHgVRbltHJWUlER8fDxHjhzpVPSMjAxefvllFEVh+fLlHuv1NZ21rb+j+Vpx48aNKIpCXl4eR44cYerUqbfVmTdvHrt27QLgscce6+u2DSx8SQ+1tbUSHR0tu3btkhUrVkhqaqrY7fbbjrl06ZLExMRITExMv017t7bNX/Ap9T3zzDNcvXqVXbt24XA4GD9+PHPnzuXVV1+97bgpU6ZgsVjYv39/X38HPeKPqa9bfZQvPPTQQyxYsIDHH3+8r9vmudF+KJTPfVRXXLhwge3bt3P27FkeeeSRvm7XgKPXZibsdjvNzc188skn6PX6bx8wQAd6PfX5A/7YtsBcn5/gtY/yR4NtoBJweP2EQOrzE/xSKLvdzrVr1zyW19bW4nA4+vo0exW/FOpnP/sZ+fn5Hss///xzXnnllb4+zV7F74Q6e/YsBQUFZGRkeKwza9YsPv74Y06dOtXXp9tr+CzUnj17yM7OJjExkQULFlBdXQ3AV199xZIlS3jttddITk5mwoQJnDx5ssNx48ePJzMzk5ycHBYtWgTA3/72tw7TTMePH2fBgm9eHfeHP/yB9PR0hg0bxu9+9zv3/t/+9rf86Ec/Arw7z4sWLeL111/v6+vbe/gyw+xyuSQtLU127dollZWV8uSTT8rPf/5zERH57LPPRNM0ef7556WgoEDmzJkjs2fPFhGRxsZGCQ0NlU2bNklubq6MHj1ahg8fLiIiBw8elPT0dPdnHDhwQCZMmCAiImfPnpX09HQpLS2VQ4cOSXx8vBQUFIiIyJgxY+TYsWMiIlJVVSURERGydetWee+992TYsGHS0NAgIiK5ubmSmJjYZdv8BZ+EamhokEOHDomIiN1ul1dffVXuv/9+t1ARERHicDhEROTIkSMyYsQIERHZvXu3LFy40B1nzZo1kpKSIiLehdq/f79ERUXJiRMnRETk8uXLYrPZxOl0islkkqqqKvdxnpzn4uJiAaSurs5r2/wFn1Kf2Wzm+PHjjBo1iqSkJLc52E50dDSq2vZOmuDgYPdra3JzcxkxYoS73pQpUzx+xs1PadOnT2fRokVkZWWRkpLCn//8Z4KDgykpKcHlchEZGemu+9RTTyEiDB06lPvuu8+9PyEhAUVRuHHjRl8nrV7BJ6EOHz7Ma6+9xu7duykvL2fZsmUdBo06XedhVFWlpKTEvV1eXt6h/OZXDJSUlLgH2DabjV/+8pdUVVWxatUq3nnnHXbs2IGmabS0tHR4NL/VeW6npqYGo9FITExMX1/jXsEnofLz8xkzZgwpKSk4HA42btzo06zF1KlT2bdvH5cvX8bpdLJq1Sp3WVJSEpcuXeLixYu4XC42bNjgLtu8eTPPPfccer2emTNnMnHiRGpraxkyZAhWq5Xz588DcO3aNZYtW8aqVat45ZVXWLp0Ke0v2y8uLmbUqFEev0T+hk+tmDdvHhcvXmTChAmkp6fzve99jxMnTrBjxw6vx82ZM4elS5eSnZ1NcnIysbGx7lfeDB06lOnTp5OamkpaWhrJyckdPu/QoUMkJyeTkZFBWVkZ8+fPR1EUMjMz3UL99Kc/ZdKkScyePZsXXngBTdP4zW9+A7T5Y2lpaX19fXsPT51XZ0Xnz5+X1tZWERGx2WzS1NTktQOsrKyUgoICcTgc4nQ6JTc3Vx599NEOdSoqKqSlpeW2Y+12u+Tl5UlFRUWH/Tt37pR58+Z12fnOmzev05+1eWpbf6dbQnWXsrIySUxMlDVr1si2bdtkzJgxsmnTpm8d97777pPCwkKP5UVFRTJr1izPjfZDof7uxuHx48fZsWMHDQ0NPPDAAx2ezHrKxYsXqaqqYtKkSZ2WHzt2jKioKIYOHdppuT8ahwGH108YGI9E3wF6LFRv/Z9T30XLoif0SKhLly6RkpLSKyfwXbQsekKfpr7vqmXRE3wW6oMPPmDixIlMmjSJbdu2dSjbt28f6enphIaGMnfuXCorK91lnmwO6GhZeFsIN+Asi57gy1ijpqZGgoODZcWKFXLw4EEZO3asxMfHi0jbuqiwsDDZt2+fVFVVyY9//GOZOXOmiHi3OUQ6WhYrV650HyciMnv2bHn99ddFxLtl0RPww3GUT0Jt3rxZpk2b5t7OyclxC/XrX/+6wwWuqKgQQGw2m1eb41bLwttCOG+WRY8a7YdC+fTb8wMHDnRYD3WzXVFcXMzkyZPd29HR0VgsFqqqqrzaHLdaFgkJCYwZM4bc3FwURWHs2LEMGTLEXdZuWYSEhPR1EuoTfBIqOTmZvLw893ZhYaH732lpaR06+itXrmCxWEhOTvZqc9xsWYSHhwOeF8INNMuiR/iSHgoKCiQ+Pt49Kbtw4UJ36issLJTExES5ePGiiIi88cYb8sQTT4iIyNatWyUxMVFKSkrE4XDIww8/7E59LpdLrFaru48S8bwQ7ujRozJ27NheSyMM1NQ3cuRIsrOzSU1NJS4ujgcffNBdNnz4cGbMmMHIkSMZP348FRUVbN++HWizOU6fPk12djYOh4OZM2e6LYqbLYv2ObvExESSkpKwWCzutAcD0LLoCd351hUXF99mO7RTVlYmZ86ccf92QqRrm6Mzy2L27NmyYcOGDvu8WRY9AT+8o/rc5mi3LIqKiuT3v/+9pKSkdPCnurIsetRoPxSqz22OdssiODiYbdu2sXjx4g5pryvLoif44+x5wObwEwI2h5/Qb4Tqyu7oLgPNHuk3QnVld3SXgWaP9AuhfLE7ustAs0d8FsqTlbF48WL27t0LwNatW8nMzHT/AnbZsmV89NFHXa748HWFRmd8Z+wRX8Ya3qyMn/zkJ/Liiy+KiMjSpUtF0zTJy8sTEZHBgwdLeXm51xUfIr6v0OiMntgj+OE4yiehvFkZe/bskYyMDBERSU9PlyeffFLefPNNOXPmjHu1hrcVH91ZodEZPbFH/FEon1KfNysjKyuLU6dOUVlZiYgwZ84cPvvsMw4fPsyMGTM6HNPZio/urNDojJvtkdzcXI/2iL/jk1BpaWmUlpa6t2+2MoKCgpgwYQJvvPEGU6dOJSsryy3Uvffe+80HefixfndWaHii3R7ZuXPnwLVHPN1qNxd5szJERH71q19JZGSkvP322yIikpqaKjExMVJfXy8ibanv5kVrJ0+edNskt9od3t4NuH79eqmsrLztXLtrjzBQU9/NVkZGRgbLly/npZdecpfPmDGD6upqMjMzAcjKymLkyJFYLJYuY3dnhcYTTzzB2bNnb4vRbo/ceeedA9ce8aRgZ0WdWRm9ga8rNJYvXy4lJSWdlnXHHmGg3lHtxMbGkpqa6n4o6C0eeughbDab+67yRFBQEAkJCR32XbhwgZUrV972nsALFy7Q2NjYK4sS+gP9YmYCYPXq1V3O9XX2wntP7wmsrq7usMLR3wnYHP8fOXfuXI+P7bVXlQbwjZEjR/bouMD7+vwEj0IN1LTnbxQVFZGSktJ/HiYC3E5RURGbN28GAn1Uv+X8+fO8//77PP3000A/ejwP8A03ixQVFQUEhOp3nDt3roNIRUVFQECofkV+fj5bt27tIFKgj+pn5Ofns337drdIhYWFbNmyJdBH9Se8iRToo/oJZ86c8SpS+1q0gFB9SGFhITt37vQq0pYtW4CAUH2GJ1E89VEeZ88D9D7nzp3r8aTs/wMiKv1why7zBAAAAC56VFh0Y3JlYXRlLWRhdGUAAHjaMzIwsNA1NNQ1Mg8xNLIyNLAyNdE2MLAyMAAAQZQFCmijYX4AAAAuelRYdG1vZGlmeS1kYXRlAAB42jMyMLDQNTTUNTIPMTSyMjSwMjXRNjCwMjAAAEGUBQoKm5aBAAAAIHpUWHR0aWZmOnJvd3MtcGVyLXN0cmlwAAB42jM2sAQAATUAnTAwbcAAAAAASUVORK5CYII="
    }
   },
   "cell_type": "markdown",
   "id": "c1b2da67",
   "metadata": {},
   "source": [
    "![66d94cb86ab90a95cfe745d9613c37b1.png](attachment:66d94cb86ab90a95cfe745d9613c37b1.png)\n",
    "\n",
    "图 5.2：DRS截图\n",
    "\n",
    "我们讨论[5.1](https://usyiyi.github.io/nlp-py-2e-zh/ch10.html#fig-drs1)中DRS的真值条件时，假设最上面的段落指称被解释为存在量词，而条件也进行了解释，虽然它们是联合的。事实上，每一个DRS都可以转化为一阶逻辑公式，`fol()`方法实现这种转换。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "b6b8bf7d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "exists x y.(angus(x) & dog(y) & own(x,y))\n"
     ]
    }
   ],
   "source": [
    "print(drs1.fol())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6cdb13d3",
   "metadata": {},
   "source": [
    "作为一阶逻辑表达式功能补充，DRT`表达式`有DRS-连接运算符，用`+`符号表示。两个DRS的连接是一个单独的DRS包含合并的段落指称和来自两个论证的条件。DRS-连接自动进行α-转换绑定变量避免名称冲突。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "d1706e17",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(([x],[walk(x)]) + ([y],[run(y)]))\n"
     ]
    }
   ],
   "source": [
    "drs2 = read_dexpr('([x], [walk(x)]) + ([y], [run(y)])')\n",
    "print(drs2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "a162db99",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([x,y],[walk(x), run(y)])\n"
     ]
    }
   ],
   "source": [
    "print(drs2.simplify())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "05fda427",
   "metadata": {},
   "source": [
    "虽然迄今为止见到的所有条件都是原子的，一个DRS可以内嵌入另一个DRS，这是全称量词被处理的方式。在`drs3`中，没有顶层的段落指称，唯一的条件是由两个子DRS组成，通过蕴含连接。再次，我们可以使用`fol()`来获得真值条件的句柄。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "7e0bf0cb",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "all x.(dog(x) -> exists y.(ankle(y) & bite(x,y)))\n"
     ]
    }
   ],
   "source": [
    "drs3 = read_dexpr('([], [(([x], [dog(x)]) -> ([y],[ankle(y), bite(x, y)]))])')\n",
    "print(drs3.fol())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "91825803",
   "metadata": {},
   "source": [
    "我们较早前指出DRT旨在通过链接照应代词和现有的段落指称来解释照应代词。DRT设置约束条件使段落指称可以像先行词那样“可访问”，但并不打算解释一个特殊的先行词如何被从候选集合中选出的。模块`nltk.sem.drt_resolve_anaphora`采用了类此的保守策略：如果DRS包含`PRO(x)`形式的条件，方法`resolve_anaphora()`将其替换为`x = [...]`形式的条件，其中`[...]`是一个可能的先行词列表。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "c357aa77",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([u,x,y,z],[angus(x), dog(y), own(x,y), PRO(u), irene(z), bite(u,z)])\n"
     ]
    }
   ],
   "source": [
    "drs4 = read_dexpr('([x, y], [angus(x), dog(y), own(x, y)])')\n",
    "drs5 = read_dexpr('([u, z], [PRO(u), irene(z), bite(u, z)])')\n",
    "drs6 = drs4 + drs5\n",
    "print(drs6.simplify())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "7b7db772",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([u,x,y,z],[angus(x), dog(y), own(x,y), (u = [x,y,z]), irene(z), bite(u,z)])\n"
     ]
    }
   ],
   "source": [
    "print(drs6.simplify().resolve_anaphora())"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e7f46dca",
   "metadata": {},
   "source": [
    "由于指代消解算法已分离到它自己的模块，这有利于在替代程序中交换，使对正确的先行词的猜测更加智能。\n",
    "\n",
    "我们对DRS的处理与处理λ-抽象的现有机制是完全兼容的，因此可以直接基于DRT而不是一阶逻辑建立组合语义表示。这种技术在下面的不确定性规则（是语法`drt.fcfg`的一部分）中说明。为便于比较，我们已经从`simple-sem.fcfg`增加了不确定性的平行规则。\n",
    "\n",
    "> Det[num=sg,SEM=<\\P Q.(([x],[]) + P(x) + Q(x))>] -> 'a'\n",
    "> \n",
    "> Det[num=sg,SEM=<\\P Q. exists x.(P(x) & Q(x))>] -> 'a'\n",
    "\n",
    "## 5.2 段落处理\n",
    "\n",
    "我们解释一句话时会使用丰富的上下文知识，一部分取决于前面的内容，一部分取决于我们的背景假设。DRT提供了一个句子的含义如何集成到前面段落表示中的理论，但是在前面的讨论中明显缺少这两个部分。首先，一直没有尝试纳入任何一种推理；第二，我们只处理了个别句子。这些遗漏由模块`nltk.inference.discourse`纠正。\n",
    "\n",
    "段落是一个句子的序列s1, sn，段落线是读法的序列s1-ri, sn-rj ，每个序列对应段落中的一个句子。该模块按增量处理句子，当有歧义时保持追踪所有可能的线。为简单起见，下面的例子中忽略了范围歧义。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "0bbdf4e2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "s0 readings:\n",
      "\n",
      "s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "\n",
      "s1 readings:\n",
      "\n",
      "s1-r0: all z1.(student(z1) -> person(z1))\n"
     ]
    }
   ],
   "source": [
    "dt = nltk.DiscourseTester(['A student dances', 'Every student is a person'])\n",
    "dt.readings()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2b4521a7",
   "metadata": {},
   "source": [
    "一个新句子添加到当前的段落时，设置参数`consistchk=True`会通过每条线，即每个可接受的读法的序列的检查模块来检查一致性。在这种情况下，用户可以选择收回有问题的句子。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "id": "0d0604f0",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Inconsistent discourse: d0 ['s0-r0', 's1-r0', 's2-r0']:\n",
      "    s0-r0: exists z1.(student(z1) & dance(z1))\n",
      "    s1-r0: all z1.(student(z1) -> person(z1))\n",
      "    s2-r0: -exists z1.(person(z1) & dance(z1))\n",
      "\n"
     ]
    }
   ],
   "source": [
    "dt.add_sentence('No person dances', consistchk=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "2b608e13",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Current sentences are \n",
      "s0: A student dances\n",
      "s1: Every student is a person\n"
     ]
    }
   ],
   "source": [
    "dt.retract_sentence('No person dances', verbose=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "4690775b",
   "metadata": {},
   "source": [
    "以类似的方式，我们使用`informchk=True`检查新的句子φ是否对当前的段落有信息量。定理证明器将段落线中现有的句子当做假设，尝试证明φ；如果没有发现这样的证据，那么它是有信息量的。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "4909269f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Sentence 'A person dances' under reading 'exists x.(person(x) & dance(x))':\n",
      "Not informative relative to thread 'd0'\n"
     ]
    }
   ],
   "source": [
    "dt.add_sentence('A person dances', informchk=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "39256ad1",
   "metadata": {},
   "source": [
    "也可以传递另一套假设作为背景知识，并使用这些筛选出不一致的读法；详情请参阅`http://nltk.org/howto`上的段落HOWTO。\n",
    "\n",
    "`discourse`模块可适应语义歧义，筛选出不可接受的读法。下面的例子调用Glue语义和DRT。由于Glue语义模块被配置为使用的覆盖面广的Malt 依存关系分析器，输入（Every dog chases a boy. He runs.）需要分词和标注。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "2b1e0abc",
   "metadata": {
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "\n",
      "s0 readings:\n",
      "\n",
      "s0-r0: exists z1.(dog(z1) & exists z3.(boy(z3) & chase(z1,z3) & all z2.(boy(z2) -> (z3 = z2))))\n",
      "\n",
      "s1 readings:\n",
      "\n",
      "s1-r0: exists z1.(boy(z1) & dance(z1) & all z2.(boy(z2) -> (z1 = z2)))\n"
     ]
    }
   ],
   "source": [
    "import nltk\n",
    "from nltk.tag import RegexpTagger\n",
    "tagger = RegexpTagger([\n",
    "    ('^(chases|runs)$', 'VB'),\n",
    "    ('^(a)$', 'ex_quant'),\n",
    "    ('^(every)$', 'univ_quant'),\n",
    "    ('^(dog|boy)$', 'NN'),\n",
    "    ('^(He)$', 'PRP')\n",
    "])\n",
    "from nltk.parse import malt\n",
    "mp = malt.MaltParser('D:\\maltparser-1.7', 'D:\\engmalt.linear-1.7.mco', tagger=tagger) # 设置环境变量或者使用文件路径，请在 asset/ 内下载相关内容\n",
    "rc = nltk.DrtGlueReadingCommand(depparser=mp)\n",
    "# dt = nltk.DiscourseTester(['Every dog chases a boy', 'boy runs']) # 添加自定义 tagger 无效\n",
    "dt = nltk.DiscourseTester(['A dog chases the boy', 'the boy dances'])\n",
    "dt.readings()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "21f6a39d",
   "metadata": {},
   "source": [
    "<!--\n",
    "s0 readings:\n",
    "\n",
    "s0-r0: ([],[(([x],[dog(x)]) -> ([z3],[boy(z3), chases(x,z3)]))])\n",
    "s0-r1: ([z4],[boy(z4), (([x],[dog(x)]) -> ([],[chases(x,z4)]))])\n",
    "\n",
    "s1 readings:\n",
    "\n",
    "s1-r0: ([x],[PRO(x), runs(x)])\n",
    "-->\n",
    "段落的第一句有两种可能的读法，取决于量词的作用域。第二句的唯一的读法通过条件PRO(x)`表示代词He。现在让我们看看段落线的结果："
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "d0b3c35c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "d0: ['s0-r0', 's1-r0', 's2-r0'] : (exists z1.(student(z1) & dance(z1)) & all z1.(student(z1) -> person(z1)) & exists z1.(person(z1) & dance(z1)))\n"
     ]
    }
   ],
   "source": [
    "dt.readings(show_thread_readings=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0a109bcb",
   "metadata": {},
   "source": [
    "当我们检查段落线`d0`和`d1`时，我们看到读法`s0-r0`，其中every dog超出了`a boy`的范围，被认为是不可接受的，因为第二句的代词不能得到解释。相比之下，段落线`d1`中的代词（重写为`z24`）*通过*等式`(z24 = z20)`绑定。\n",
    "\n",
    "不可接受的读法可以通过传递参数`filter=True`过滤掉。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "631f78ff",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "d0: ['s0-r0', 's1-r0', 's2-r0'] : (exists z1.(student(z1) & dance(z1)) & all z1.(student(z1) -> person(z1)) & exists z1.(person(z1) & dance(z1)))\n"
     ]
    }
   ],
   "source": [
    "dt.readings(show_thread_readings=True, filter=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "636cc3f6",
   "metadata": {},
   "source": [
    "虽然这一小段是极其有限的，它应该能让你对于我们在超越单个句子后产生的语义处理问题，以及部署用来解决它们的技术有所了解。\n",
    "\n",
    "## 6 小结\n",
    "\n",
    "- 一阶逻辑是一种适合在计算环境中表示自然语言的含义的语言，因为它很灵活，足以表示自然语言含义的很多有用的方面，具有使用一阶逻辑推理的高效的定理证明器。（同样的，自然语言语义中也有各种各样的现象，需要更强大的逻辑机制。）\n",
    "- 在将自然语言句子翻译成一阶逻辑的同时，我们可以通过检查一阶公式模型表述这些句子的真值条件。\n",
    "- 为了构建成分组合的意思表示，我们为一阶逻辑补充了λ-演算。\n",
    "- λ-演算中的β-约简在语义上与函数传递参数对应。句法上，它包括将被函数表达式中的λ绑定的变量替换为函数应用中表达式提供的参数。\n",
    "- 构建模型的一个关键部分在于建立估值，为非逻辑常量分配解释。这些被解释为*n*元谓词或独立常量。\n",
    "- 一个开放表达式是一个包含一个或多个自由变量的表达式。开放表达式只在它的自由变量被赋值时被解释。\n",
    "- 量词的解释是对于具有变量x的公式φ[x]，构建个体的集合，赋值*g*分配它们作为x的值使φ[x]为真。然后量词对这个集合加以约束。\n",
    "- 一个封闭的表达式是一个没有自由变量的表达式；也就是，变量都被绑定。一个封闭的表达式是真是假取决于所有变量赋值。\n",
    "- 如果两个公式只是由绑定操作符（即λ或量词）绑定的变量的标签不同，那么它们是α-等价。重新标记公式中的绑定变量的结果被称为α-转换。\n",
    "- 给定有两个嵌套量词*Q*1和*Q*2的公式，最外层的量词*Q*1有较广的范围（或范围超出*Q*2）。英语句子往往由于它们包含的量词的范围而产生歧义。\n",
    "- 在基于特征的语法中英语句子可以通过将`sem`作为特征与语义表达关联。一个复杂的表达式的`sem`值通常包括成分表达式的`sem`值的函数应用。\n",
    "\n",
    "## 7 深入阅读\n",
    "\n",
    "关于本章的进一步材料以及如何安装Prover9定理证明器和Mace4模型生成器的内容请查阅`http://nltk.org/`。这两个推论工具一般信息见[(McCune, 2008)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#mccune)。\n",
    "\n",
    "用NLTK进行语义分析的更多例子，请参阅`http://nltk.org/howto`上的语义和逻辑HOWTO。请注意，范围歧义还有其他两种解决方法，即[(Blackburn & Bos, 2005)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#blackburn2005rin)描述的Hole语义和[(Dalrymple, 1999)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#dalrymple:1999:rrb)描述的Glue语义。\n",
    "\n",
    "自然语言语义中还有很多现象没有在本章中涉及到，主要有：\n",
    "\n",
    "1. 事件、时态和体；\n",
    "2. 语义角色；\n",
    "3. 广义量词，如most；\n",
    "4. 内涵结构，例如像may和believe这样的动词。\n",
    "\n",
    "（1）和（2）可以使用一阶逻辑处理，（3）和（4）需要不同的逻辑。下面的读物中很多都讲述了这些问题。\n",
    "\n",
    "建立自然语言前端数据库方面的结果和技术的综合概述可以在[(Androutsopoulos, Ritchie, & Thanisch, 1995)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#androutsopoulos1995nli)中找到。\n",
    "\n",
    "任何一本现代逻辑的入门书都将提出命题和一阶逻辑。强烈推荐[(Hodges, 1977)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#hodges1977l)，书中有很多有关自然语言的有趣且有洞察力的文字和插图。\n",
    "\n",
    "要说范围广泛，参阅两卷本的关于逻辑教科书[(Gamut, 1991)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#gamut1991il)和[(Gamut, 1991)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#gamut1991illg)，也包含了有关自然语言的形式语义的当代材料，例如Montague文法和内涵逻辑。[(Kamp & Reyle, 1993)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#kampreyle1993)提供段落表示理论的权威报告，包括涵盖大量且有趣的自然语言片段，包括时态、体和形态。另一个对许多自然语言结构的语义的全面研究是[(Carpenter, 1997)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#carpenter1997tls)。\n",
    "\n",
    "有许多作品介绍语言学理论框架内的逻辑语义。[(Chierchia & McConnell-Ginet, 1990)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#chierchia1990mg)与句法相对无关，而[(Heim & Kratzer, 1998)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#heim1998sgg) and [(Larson & Segal, 1995)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#larson1995km)都更明确的倾向于将语义真值条件整合到乔姆斯基框架中。\n",
    "\n",
    "[(Blackburn & Bos, 2005)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#blackburn2005rin)是致力于计算语义的第一本教科书，为该领域提供了极好的介绍。它扩展了许多本章涵盖的主题，包括量词范围歧义的未指定、一阶逻辑推理以及段落处理。\n",
    "\n",
    "要获得更先进的当代语义方法的概述，包括处理时态和广义量词，尝试查阅[(Lappin, 1996)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#lappin1996hcs)或[(Benthem & Meulen, 1997)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#vanbenthem1997hll)。\n",
    "\n",
    "## 8 练习\n",
    "\n",
    "1. ☼ 将下列句子翻译成命题逻辑，并用`Expression.fromstring()`验证结果。提供显示你的翻译中命题变量如何对应英语表达的一个要点。\n",
    "\n",
    "   1. If Angus sings, it is not the case that Bertie sulks.\n",
    "   2. Cyril runs and barks.\n",
    "   3. It will snow if it doesn't rain.\n",
    "   4. It's not the case that Irene will be happy if Olive or Tofu comes.\n",
    "   5. Pat didn't cough or sneeze.\n",
    "   6. If you don't come if I call, I won't come if you call.\n",
    "\n",
    "2. ☼ 翻译下面的句子为一阶逻辑的谓词参数公式。\n",
    "\n",
    "   1. Angus likes Cyril and Irene hates Cyril.\n",
    "   2. Tofu is taller than Bertie.\n",
    "   3. Bruce loves himself and Pat does too.\n",
    "   4. Cyril saw Bertie, but Angus didn't.\n",
    "   5. Cyril is a fourlegged friend.\n",
    "   6. Tofu and Olive are near each other.\n",
    "\n",
    "3. ☼ 翻译下列句子为成一阶逻辑的量化公式。\n",
    "\n",
    "   1. Angus likes someone and someone likes Julia.\n",
    "   2. Angus loves a dog who loves him.\n",
    "   3. Nobody smiles at Pat.\n",
    "   4. Somebody coughs and sneezes.\n",
    "   5. Nobody coughed or sneezed.\n",
    "   6. Bruce loves somebody other than Bruce.\n",
    "   7. Nobody other than Matthew loves somebody Pat.\n",
    "   8. Cyril likes everyone except for Irene.\n",
    "   9. Exactly one person is asleep.\n",
    "\n",
    "4. ☼ 翻译下列动词短语，使用λ-抽象和一阶逻辑的量化公式。\n",
    "\n",
    "   1. feed Cyril and give a capuccino to Angus\n",
    "   2. be given 'War and Peace' by Pat\n",
    "   3. be loved by everyone\n",
    "   4. be loved or detested by everyone\n",
    "   5. be loved by everyone and detested by no-one\n",
    "\n",
    "5. ☼ 思考下面的语句：\n",
    "\n",
    "   ```\n",
    "   >>> read_expr = nltk.sem.Expression.fromstring\n",
    "   >>> e2 = read_expr('pat')\n",
    "   >>> e3 = nltk.sem.ApplicationExpression(e1, e2)\n",
    "   >>> print(e3.simplify())\n",
    "   exists y.love(pat, y)\n",
    "   ```\n",
    "\n",
    "   显然这里缺少了什么东西，即`e1`值的声明。为了`ApplicationExpression(e1, e2)`被β-转换为`exists y.love(pat, y)`，`e1`必须是一个以`pat`为参数的λ-抽象。你的任务是构建这样的一个抽象，将它绑定到`e1`，使上面的语句都是满足（上到字母方差）。此外，提供一个`e3.simplify()`的非正式的英文翻译。\n",
    "\n",
    "   现在根据`e3.simplify()`的进一步情况（如下所示）继续做同样的任务。\n",
    "\n",
    "   ```\n",
    "   >>> print(e3.simplify())\n",
    "   exists y.(love(pat,y) | love(y,pat))\n",
    "   ```\n",
    "\n",
    "   ```\n",
    "   >>> print(e3.simplify())\n",
    "   exists y.(love(pat,y) | love(y,pat))\n",
    "   ```\n",
    "\n",
    "   ```\n",
    "   >>> print(e3.simplify())\n",
    "   walk(fido)\n",
    "   ```\n",
    "\n",
    "6. ☼ 如前面的练习中那样，找到一个λ-抽象`e1`，产生与下面显示的等效的结果。\n",
    "\n",
    "   ```\n",
    "   >>> e2 = read_expr('chase')\n",
    "   >>> e3 = nltk.sem.ApplicationExpression(e1, e2)\n",
    "   >>> print(e3.simplify())\n",
    "   \\x.all y.(dog(y) -> chase(x,pat))\n",
    "   ```\n",
    "\n",
    "   ```\n",
    "   >>> e2 = read_expr('chase')\n",
    "   >>> e3 = nltk.sem.ApplicationExpression(e1, e2)\n",
    "   >>> print(e3.simplify())\n",
    "   \\x.exists y.(dog(y) & chase(pat,x))\n",
    "   ```\n",
    "\n",
    "   ```\n",
    "   >>> e2 = read_expr('give')\n",
    "   >>> e3 = nltk.sem.ApplicationExpression(e1, e2)\n",
    "   >>> print(e3.simplify())\n",
    "   \\x0 x1.exists y.(present(y) & give(x1,y,x0))\n",
    "   ```\n",
    "\n",
    "7. ☼ 如前面的练习中那样，找到一个λ-抽象`e1`，产生与下面显示的等效的结果。\n",
    "\n",
    "   ```\n",
    "   >>> e2 = read_expr('bark')\n",
    "   >>> e3 = nltk.sem.ApplicationExpression(e1, e2)\n",
    "   >>> print(e3.simplify())\n",
    "   exists y.(dog(x) & bark(x))\n",
    "   ```\n",
    "\n",
    "   ```\n",
    "   >>> e2 = read_expr('bark')\n",
    "   >>> e3 = nltk.sem.ApplicationExpression(e1, e2)\n",
    "   >>> print(e3.simplify())\n",
    "   bark(fido)\n",
    "   ```\n",
    "\n",
    "   ```\n",
    "   >>> e2 = read_expr('\\\\P. all x. (dog(x) -> P(x))')\n",
    "   >>> e3 = nltk.sem.ApplicationExpression(e1, e2)\n",
    "   >>> print(e3.simplify())\n",
    "   all x.(dog(x) -> bark(x))\n",
    "   ```\n",
    "\n",
    "8. ◑ 开发一种方法，翻译英语句子为带有二元广义量词的公式。在此方法中，给定广义量词`Q`，量化公式的形式为`Q(A, B)`，其中`A`和`B`是〈*e*, *t*〉类型的表达式。那么，例如`all(A, B)`为真当且仅当`A`表示的是`B`所表示的一个子集。\n",
    "\n",
    "9. ◑ 扩展前面练习中的方法，使量词如most和exactly three的真值条件可以在模型中计算。\n",
    "\n",
    "10. ◑ 修改`sem.evaluate`代码，使它能提供一个有用的错误消息，如果一个表达式不在模型的估值函数的域中。\n",
    "\n",
    "11. ★ 从儿童读物中选择三个或四个连续的句子。一个例子是`nltk.corpus.gutenberg`中的故事集：`bryant-stories.txt`，`burgess-busterbrown.txt`和`edgeworth-parents.txt`。开发一个语法，能将你的句子翻译成一阶逻辑，建立一个模型，使它能检查这些翻译为真或为假。\n",
    "\n",
    "12. ★ 实施前面的练习，但使用DRT作为意思表示。\n",
    "\n",
    "13. ★ 以[(Warren & Pereira, 1982)](https://usyiyi.github.io/nlp-py-2e-zh/bibliography.html#warren1982eea)为出发点，开发一种技术，转换一个自然语言查询为一种可以更加有效的在模型中评估的形式。例如，给定一个`(P(x) & Q(x))`形式的查询，将它转换为`(Q(x) & P(x))`，如果`Q`的范围比`P`小。\n",
    "\n",
    "关于本文档...\n",
    "\n",
    "针对NLTK 3.0 作出更新。本章来自于*Natural Language Processing with Python*，[Steven Bird](http://estive.net/), [Ewan Klein](http://homepages.inf.ed.ac.uk/ewan/) 和[Edward Loper](http://ed.loper.org/)，Copyright © 2014 作者所有。本章依据*Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License* [http://creativecommons.org/licenses/by-nc-nd/3.0/us/] 条款，与*自然语言工具包* [`http://nltk.org/`] 3.0 版一起发行。\n",
    "\n",
    "本文档构建于星期三 2015 年 7 月 1 日 12:30:05 AEST"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python [conda env:.conda-nltk38]",
   "language": "python",
   "name": "conda-env-.conda-nltk38-py"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.16"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}
